$\forall$$T$:Type, $X$:MaInterface($T$). ma{-}interface{-}inr($X$) $\in$ MaInterface(\{$x$:Top + $T$$\mid$ $\neg$($\uparrow$isl($x$))\} )